
#include "Formula.h"
#include "Clause.h"
#include "Literal.h"

#include <iostream>


int main(){

	bool x1 = true;
	bool x2 = true;
	bool x3 = true;

	Literal l1(&x1,false);
	Literal l2(&x2,false);
	Literal l3(&x3,false);

	Clause c1;
	c1.addLiteral(l1);
	c1.addLiteral(l2);
	c1.addLiteral(l3);

	Formula f1;
	f1.addClause(c1);

	std::cout<< "f1: " << f1.evaluate() << std::endl;


	x1 = false;

	std::cout<< "f1: " << f1.evaluate() << std::endl;

	x2 = false;
	x3 = false;

	std::cout<< "f1: " << f1.evaluate() << std::endl;



	Clause c2;
	c2.addLiteral(l1);
	c2.addLiteral(l2);
	c2.addLiteral(l3);

	x3 = true;

	std::cout<< "f1: " << f1.evaluate() << std::endl;

	Clause c3;
	Literal l4(&x1,true);
	c3.addLiteral(l4);

	f1.addClause(c3);

	std::cout<< "f1: " << f1.evaluate() << std::endl;

	x1 = true;

	std::cout<< "f1: " << f1.evaluate() << std::endl;

	return 0;
}








